Inference at * 1 2 
Iof proof for Lemma branch-ifthenelse:



1. b : 
2. P : Top
3. Q : Top
4. y : (b)
5. bool-decider(b) = (inr y )
  Q ~ if b then P else Q fi  

latex

 by AutoBoolCase b 

latex

 .

Definitions	left + right, Unit, P  Q, P & Q, x:A  B(x), x:AB(x), , s = t, b, b, x:A. B(x), t  T, , A, P  Q, False
Lemmas	eqtt to assert, iff transitivity, eqff to assert, assert of bnot, assert wf, bnot wf, not wf, bool wf